home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / scheme / schmrprt / r399rs.lha / sem.tex (.txt) < prev    next >
Encoding:
LaTeX Document  |  1989-08-31  |  23.6 KB  |  575 lines
  1. %\vfill\eject
  2. \section{Formal semantics}
  3. \label{formalsemanticssection}
  4. \bgroup
  5. \newcommand{\sembrack}[1]{[\![#1]\!]}
  6. \newcommand{\fun}[1]{\hbox{\it #1}}
  7. \newenvironment{semfun}{\begin{tabbing}$}{$\end{tabbing}}
  8. \newcommand\LOC{{\tt{}L}}
  9. \newcommand\NAT{{\tt{}N}}
  10. \newcommand\TRU{{\tt{}T}}
  11. \newcommand\SYM{{\tt{}Q}}
  12. \newcommand\CHR{{\tt{}H}}
  13. \newcommand\NUM{{\tt{}R}}
  14. \newcommand\FUN{{\tt{}F}}
  15. \newcommand\EXP{{\tt{}E}}
  16. \newcommand\STV{{\tt{}E}}
  17. \newcommand\STO{{\tt{}S}}
  18. \newcommand\ENV{{\tt{}U}}
  19. \newcommand\ANS{{\tt{}A}}
  20. \newcommand\ERR{{\tt{}X}}
  21. \newcommand\EC{{\tt{}K}}
  22. \newcommand\CC{{\tt{}C}}
  23. \newcommand\MSC{{\tt{}M}}
  24. \newcommand\PAI{\hbox{\EXP$_{\rm p}$}}
  25. \newcommand\VEC{\hbox{\EXP$_{\rm v}$}}
  26. \newcommand\STR{\hbox{\EXP$_{\rm s}$}}
  27. \newcommand\elt{\downarrow}
  28. \newcommand\drop{\dagger}
  29. %\newcommand\injekt{\hbox{ \rm in }}
  30. %\newcommand\projekt{\,\vert\,}
  31. This section provides a formal denotational semantics for the primitive
  32. expressions of Scheme and selected built-in procedures.  The concepts
  33. and notation used here are described in~\cite{Stoy77}; the notation is
  34. summarized below:
  35. \begin{tabular}{ll}
  36. $\langle\,\ldots\,\rangle$ & sequence formation \\
  37. $s \elt k$               & $k$th member of the sequence $s$ (1-based) \\
  38. $\#s$               & length of sequence $s$ \\
  39. $s \:\S\: t$               & concatenation of sequences $s$ and $t$ \\
  40. $s \drop k$                & drop the first $k$ members of sequence $s$ \\
  41. $t \rightarrow a, b$       & McCarthy conditional ``if $t$ then $a$ else $b$'' \\
  42. $\rho[x/i]$               & substitution ``$\rho$ with $x$ for $i$'' \\
  43. $x\hbox{ \rm in }{\tt{}D}$         & injection of $x$ into domain ${\tt{}D}$ \\
  44. $x\,\vert\,{\tt{}D}$       & projection of $x$ to domain ${\tt{}D}$
  45. \end{tabular}
  46. The reason that expression continuations take sequences of values instead
  47. of single values is to simplify the formal treatment of procedure calls
  48. and to make it easy to add multiple return values.
  49. The boolean flag associated with pairs, vectors, and strings will be true
  50. for mutable objects and false for immutable objects.
  51. The order of evaluation within a call is unspecified.  We mimic that
  52. here by applying arbitrary permutations {\it permute} and {\it
  53. unpermute}, which must be inverses, to the arguments in a call before
  54. and after they are evaluated.  This is not quite right since it suggests,
  55. incorrectly, that the order of evaluation is constant throughout a program (for
  56. any given number of arguments), but it is a closer approximation to the intended
  57. semantics than a left-to-right evaluation would be.
  58. The storage allocator {\it new} is implementation-dependent, but it must
  59. obey the following axiom:  if \hbox{$\fun{new}\:\sigma\:\elem\:\LOC$}, then
  60. $\sigma\:(\fun{new}\:\sigma\:\vert\:\LOC)\elt 2 = {\it false}$.
  61. \def\P{\hbox{\rm P}}
  62. \def\I{\hbox{\rm I}}
  63. \def\Ksem{\hbox{$\cal K$}}
  64. \def\Esem{\hbox{$\cal E$}}
  65. The definition of $\Ksem$ is omitted because an accurate definition of
  66. $\Ksem$ would complicate the semantics without being very interesting.
  67. If \P{} is a program in which all variables are defined before being
  68. referenced or assigned, then the meaning of \P{} is
  69. $$\Esem\sembrack{\hbox{\tt((\ide{lambda} (\arbno{\I}) \P')
  70. \hyper{undefined} \dotsfoo)}}$$
  71. where \arbno{\I} is the sequence of variables defined in \P, $\P'$
  72. is the sequence of expressions obtained by replacing every definition
  73. in \P{} by an assignment, \hyper{undefined} is an expression that evaluates
  74. to \fun{undefined}, and
  75. $\Esem$ is the semantic function that assigns meaning to expressions.
  76. %The semantics in this section was translated by machine from an
  77. %executable version of the semantics written in Scheme itself.
  78. %[This was once true, but then I modified the semantics without
  79. %going back to the executable version.  -- Will]
  80. \subsection{Abstract syntax}
  81. \def\K{\hbox{\rm K}}
  82. \def\I{\hbox{\rm I}}
  83. \def\E{\hbox{\rm E}}
  84. \def\C{\hbox{$\Gamma$}}
  85. \def\Con{\hbox{\rm Con}}
  86. \def\Ide{\hbox{\rm Ide}}
  87. \def\Exp{\hbox{\rm Exp}}
  88. \def\Com{\hbox{\rm Com}}
  89. \def\|{$\vert$}
  90. \begin{tabular}{r@{ }c@{ }l@{\qquad}l}
  91. \K & \elem & \Con & constants, including quotations \\
  92. \I & \elem & \Ide & identifiers (variables) \\
  93. \E & \elem & \Exp & expressions\\
  94. \C & \elem & \Com{} $=$ \Exp & commands
  95. \end{tabular}
  96. \setbox0=\hbox{\tt\Exp{} \goesto{}}  %\tt for spacing
  97. \setbox1=\hbox to 1\wd0{\hfil \|}
  98. \begin{grammar}
  99. \Exp{} \goesto{} \K{} \| \I{} \| (\E$_0$ \arbno{\E})
  100.  \copy1{} (lambda (\arbno{\I}) \arbno{\C} \E$_0$)
  101.  \copy1{} (lambda (\arbno{\I} {\bf.}\ \I) \arbno{\C} \E$_0$)
  102.  \copy1{} (lambda \I{} \arbno{\C} \E$_0$)
  103.  \copy1{} (if \E$_0$ \E$_1$ \E$_2$) \| (if \E$_0$ \E$_1$)
  104.  \copy1{} (set! \I{} \E)
  105. \end{grammar}
  106. \subsection{Domain equations}
  107. \begin{tabular}{@{}r@{ }c@{ }l@{ }l@{ }ll}
  108. $\alpha$   & \elem & \LOC & &          & locations \\
  109. $\nu$      & \elem & \NAT & &          & natural numbers \\
  110.            &       & \TRU &=& $\{$\it false, true$\}$ & booleans \\
  111.            &       & \SYM & &          & symbols \\
  112.            &       & \CHR & &          & characters \\
  113.            &       & \NUM & &          & numbers \\
  114.            &       & \PAI &=& $\LOC \times \LOC \times \TRU$  & pairs \\
  115.            &       & \VEC &=& $\arbno{\LOC} \times \TRU$ & vectors \\
  116.            &       & \STR &=& $\arbno{\LOC} \times \TRU$ & strings \\
  117.        &       & \MSC &=& \makebox[0pt][l]{$\{$\it false, true, 
  118.                                 null, undefined, unspecified$\}$} \\
  119.        &       &      & &          & miscellaneous \\
  120. $\phi$     & \elem & \FUN &=& $\LOC\times(\arbno{\EXP} \to \EC \to \CC)$
  121.                                        & procedure values \\
  122. $\epsilon$ & \elem & \EXP &=& \makebox[0pt][l]{$\SYM+\CHR+\NUM+\PAI+\VEC+\STR+\MSC+\FUN$}\\
  123.        &       &      & &          & expressed values \\
  124. %          &       & \STV &=& \EXP     & stored values \\
  125. $\sigma$   & \elem & \STO &=& $\LOC\to(\STV\times\TRU)$ & stores \\
  126. $\rho$       & \elem & \ENV &=& $\Ide\to\LOC$  & environments \\
  127. $\theta$   & \elem & \CC  &=& $\STO\to\ANS$  & command continuations \\
  128. $\kappa$   & \elem & \EC  &=& $\arbno{\EXP}\to\CC$ & expression continuations \\
  129.        &       & \ANS & &             & answers \\
  130.        &       & \ERR & &             & errors
  131. \end{tabular}
  132. \subsection{Semantic functions}
  133. \def\Ksem{\hbox{$\cal K$}}
  134. \def\Esem{\hbox{$\cal E$}}
  135. \def\Csem{\hbox{$\cal C$}}
  136. \begin{tabular}{@{}r@{ }l}
  137.   $\Ksem:$ & $\Con\to\EXP$  \\
  138.   $\Esem:$ & $\Exp\to\ENV\to\EC\to\CC$ \\
  139. $\arbno{\Esem}:$ & $\arbno{\Exp}\to\ENV\to\EC\to\CC$ \\
  140.   $\Csem:$ & $\arbno{\Com}\to\ENV\to\CC\to\CC$
  141. \end{tabular}
  142. % thin \,  medium \> [or \:]   thick \;
  143. \renewcommand{\:}{\mskip\medmuskip}
  144. \newcommand{\wrong}[1]{\fun{wrong }\hbox{\rm``#1''}}
  145. \newcommand{\go}[1]{\hbox{\hspace*{#1em}}}
  146. \bgroup\small
  147. \vspace{1ex}
  148. Definition of \Ksem{} deliberately omitted.
  149. \begin{semfun}
  150. \Esem\sembrack{\K} =
  151.   \lambda\rho\kappa\:.\:\fun{send}\,(\Ksem\sembrack{\K})\,\kappa
  152. \end{semfun}
  153. \begin{semfun}
  154. \Esem\sembrack{\I} = 
  155.   \lambda\rho\kappa\:.\:\fun{hold}\:
  156.     $\=$(\fun{lookup}\:\rho\:\I)$\\
  157.      \>$(\fun{single}(\lambda\epsilon\:.\:
  158.         $\=$\epsilon = \fun{undefined}\rightarrow$\\
  159.      \>  \> \go{2}$\wrong{undefined variable},$\\
  160.      \>  \>\go{1}$\fun{send}\:\epsilon\:\kappa))
  161. \end{semfun}
  162. \begin{semfun}
  163. \Esem\sembrack{\hbox{\tt($\E_0$ \arbno{\E})}} =$\\
  164.  \go{1}$\lambda\rho\kappa\:.\:\arbno{\Esem}
  165.     $\=$(\fun{permute}(\langle\E_0\rangle\:\S\:\arbno{\E}))$\\
  166.      \>$\rho\:$\\
  167.      \>$(\lambda\arbno{\epsilon}\:.\:
  168.         ($\=$(\lambda\arbno{\epsilon}\:.\:
  169.                  \fun{applicate}\:(\arbno{\epsilon}\elt 1)
  170.                  \:(\arbno{\epsilon}\drop 1)
  171.                 \:\kappa)$\\
  172.      \>   \>$(\fun{unpermute}\:\arbno{\epsilon})))
  173. \end{semfun}
  174. \begin{semfun}
  175. \Esem\sembrack{\hbox{\tt(\ide{lambda} (\arbno{\I}) \arbno{\C} $\E_0$)}} =$\\
  176.  \go{1}$\lambda\rho\kappa\:.\:\lambda\sigma\:.\:$\\
  177.   \go{2}$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  178.    \go{3}$\fun{send}\:
  179.      $\=$(\langle
  180.          $\=$\fun{new}\:\sigma\,\vert\,\LOC,$\\
  181.       \>  \>$\lambda\arbno{\epsilon}\kappa^\prime\:.\:
  182.            $\=$\#\arbno{\epsilon} = \#{\arbno{\I}}\rightarrow$\\
  183.       \>  \>    \>$\go{1}\fun{tievals}
  184.            $\=$(\lambda\arbno{\alpha}\:.\:
  185.              $\=$(\lambda\rho^\prime\:.\:\Csem\sembrack{\arbno{\C}}\rho^\prime
  186.                   (\Esem\sembrack{\E_0}\rho^\prime\kappa^\prime))$\\
  187.       \>  \>    \>  \>    \>$(\fun{extends}\:\rho\:{\arbno{\I}}\:\arbno{\alpha}))$\\
  188.       \>  \>    \>  \>$\arbno{\epsilon},$\\
  189.       \>  \>    \>\go{1}$\wrong{wrong number of arguments}\rangle$\\
  190.       \>  \>$\hbox{ \rm in }\EXP)$\\
  191.       \>$\kappa$\\
  192.       \>$(\fun{update}\:(\fun{new}\:\sigma\,\vert\,\LOC)
  193.                        \:\fun{unspecified}
  194.                \:\sigma),$\\
  195.   \go{3}$\wrong{out of memory}\:\sigma
  196. \end{semfun}
  197. \begin{semfun}
  198. \Esem\sembrack{\hbox{\tt(lambda (\arbno{\I} {\bf.}\ \I) \arbno{\C} $\E_0$)}} =$\\
  199.  \go{1}$\lambda\rho\kappa\:.\:\lambda\sigma\:.\:$\\
  200.   \go{2}$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  201.    \go{3}$\fun{send}\:
  202.      $\=$(\langle
  203.          $\=$\fun{new}\:\sigma\,\vert\,\LOC,$\\
  204.       \>  \>$\lambda\arbno{\epsilon}\kappa^\prime\:.\:
  205.            $\=$\#\arbno{\epsilon} \geq \#\arbno{\I}\rightarrow$\\
  206.       \>  \>    \>\go{1}$\fun{tievalsrest}$\\
  207.       \>  \>    \>\go{2}\=$(\lambda\arbno{\alpha}\:.\:
  208.                $\=$(\lambda\rho^\prime\:.\:\Csem\sembrack{\arbno{\C}}\rho^\prime
  209.                    (\Esem\sembrack{\E_0}\rho^\prime\kappa^\prime))$\\
  210.       \>  \>    \>       \> \>$(\fun{extends}\:\rho
  211.                    \:(\arbno{\I}\:\S\:\langle\I\rangle)
  212.                    \:\arbno{\alpha}))$\\
  213.       \>  \>    \>       \>$\arbno{\epsilon}$\\
  214.       \>  \>    \>       \>$(\#\arbno{\I}),$\\
  215.       \>  \>    \>\go{1}$\wrong{too few arguments}\rangle\hbox{ \rm in }\EXP)$\\
  216.       \>$\kappa$\\
  217.       \>$(\fun{update}\:(\fun{new}\:\sigma\,\vert\,\LOC)
  218.                        \:\fun{unspecified}
  219.                \:\sigma),$\\
  220.   \go{3}$\wrong{out of memory}\:\sigma
  221. \end{semfun}
  222. \begin{semfun}
  223. \Esem\sembrack{\hbox{\tt(lambda \I{} \arbno{\C} $\E_0$)}} =
  224.  \Esem\sembrack{\hbox{\tt(lambda ({\bf.}\ \I) \arbno{\C} $\E_0$)}}
  225. \end{semfun}
  226. \begin{semfun}
  227. \Esem\sembrack{\hbox{\tt(\ide{if} $\E_0$ $\E_1$ $\E_2$)}} =$\\
  228.  \go{1}$\lambda\rho\kappa\:.\:
  229.    \Esem\sembrack{\E_0}\:\rho\:(\fun{single}\:(\lambda\epsilon\:.\:
  230.     $\=$\fun{truish}\:\epsilon\rightarrow\Esem\sembrack{\E_1}\rho\kappa,$\\
  231.      \>\go{1}$\Esem\sembrack{\E_2}\rho\kappa))
  232. \end{semfun}
  233. \begin{semfun}
  234. \Esem\sembrack{\hbox{\tt(if $\E_0$ $\E_1$)}} =$\\
  235.  \go{1}$\lambda\rho\kappa\:.\:
  236.    \Esem\sembrack{\E_0}\:\rho\:(\fun{single}\:(\lambda\epsilon\:.\:
  237.     $\=$\fun{truish}\:\epsilon\rightarrow\Esem\sembrack{\E_1}\rho\kappa,$\\
  238.      \>\go{1}$\fun{send}\:\fun{unspecified}\:\kappa))
  239. \end{semfun}
  240. Here and elsewhere, any expressed value other than {\it undefined} may
  241. be used in place of {\it unspecified}.
  242. \begin{semfun}
  243. \Esem\sembrack{\hbox{\tt(\ide{set!} \I{} \E)}} =$\\
  244.  \go{1}$\lambda\rho\kappa\:.\:\Esem\sembrack{\E}\:\rho\:
  245.      (\fun{single}(\lambda\epsilon\:.\:\fun{assign}\:
  246.        $\=$(\fun{lookup}\:\rho\:\I)$\\
  247.     \>$\epsilon$\\
  248.     \>$(\fun{send}\:\fun{unspecified}\:\kappa)))
  249. \end{semfun}
  250. \begin{semfun}
  251. \arbno{\Esem}\sembrack{\:} =
  252.   \lambda\rho\kappa\:.\:\kappa\langle\:\rangle
  253. \end{semfun}
  254. \begin{semfun}
  255. \arbno{\Esem}\sembrack{\E_0\:\arbno{\E}} =$\\
  256.  \go{1}$\lambda\rho\kappa\:.\:
  257.       \Esem\sembrack{\E_0}\:\rho\:
  258.          (\fun{single}
  259.         (\lambda\epsilon_0\:.\:\arbno{\Esem}\sembrack{\arbno{\E}}
  260.         \:\rho\:(\lambda\arbno{\epsilon}\:.\:
  261.                    \kappa\:(\langle\epsilon_0\rangle\:\S\:\arbno{\epsilon}))))
  262. \end{semfun}
  263. \begin{semfun}
  264. \Csem\sembrack{\:} = \lambda\rho\theta\,.\:\theta
  265. \end{semfun}
  266. \begin{semfun}
  267. \Csem\sembrack{\C_0\:\arbno{\C}} =
  268.   \lambda\rho\theta\:.\:\Esem\sembrack{\C_0}\:\rho\:(\lambda\arbno{\epsilon}\:.\:
  269.    \Csem\sembrack{\arbno{\C}}\rho\theta)
  270. \end{semfun}
  271. \egroup  % end smallish
  272. \subsection{Auxiliary functions}
  273. \bgroup\small
  274. \begin{semfun}
  275. \fun{lookup}        :  \ENV \to \Ide \to \LOC$\\$
  276. \fun{lookup} =
  277.  \lambda\rho\I\:.\:\rho\I
  278. \end{semfun}
  279. \begin{semfun}
  280. \fun{extends}       :  \ENV \to \arbno{\Ide} \to \arbno{\LOC} \to \ENV$\\$
  281. \fun{extends} =$\\
  282.  \go{1}$\lambda\rho\arbno{\I}\arbno{\alpha}\:.\:
  283.    $\=$\#\arbno{\I}=0\rightarrow\rho,$\\
  284.     \>$\go{1}\fun{extends}\:(\rho[(\arbno{\alpha}\elt 1)/(\arbno{\I}\elt 1)])
  285.                    \:(\arbno{\I}\drop 1)
  286.                    \:(\arbno{\alpha}\drop 1)
  287. \end{semfun}
  288. \begin{semfun}
  289. \fun{wrong}  :  \ERR \to \CC    \hbox{\qquad [implementation-dependent]}
  290. \end{semfun}
  291. \begin{semfun}
  292. \fun{send}          :  \EXP \to \EC \to \CC$\\$
  293. \fun{send} =
  294.  \lambda\epsilon\kappa\:.\:\kappa\langle\epsilon\rangle
  295. \end{semfun}
  296. \begin{semfun}
  297. \fun{single}        :  (\EXP \to \CC) \to \EC$\\$
  298. \fun{single} =$\\
  299.  \go{1}$\lambda\psi\arbno{\epsilon}\:.\:
  300.    $\=$\#\arbno{\epsilon}=1\rightarrow\psi(\arbno{\epsilon}\elt 1),$\\
  301.     \>$\go{1}\wrong{wrong number of return values}
  302. \end{semfun}
  303. \begin{semfun}
  304. \fun{new}           :  \STO \to (\LOC + \{ \fun{error} \})
  305.     \hbox{\qquad [implementation-dependent]}
  306. \end{semfun}
  307. \begin{semfun}
  308. \fun{hold}          :  \LOC \to \EC \to \CC$\\$
  309. \fun{hold} =
  310.  \lambda\alpha\kappa\sigma\:.\:\fun{send}\,(\sigma\alpha\elt 1)\kappa\sigma
  311. \end{semfun}
  312. \begin{semfun}
  313. \fun{assign}        :  \LOC \to \EXP \to \CC \to \CC$\\$
  314. \fun{assign} =
  315.  \lambda\alpha\epsilon\theta\sigma\:.\:\theta(\fun{update}\:\alpha\epsilon\sigma)
  316. \end{semfun}
  317. \begin{semfun}
  318. \fun{update}        :  \LOC \to \EXP \to \STO \to \STO$\\$
  319. \fun{update} =
  320.  \lambda\alpha\epsilon\sigma\:.\:\sigma[\langle\epsilon,\fun{true}\rangle/\alpha]
  321. \end{semfun}
  322. \begin{semfun}
  323. \fun{tievals}       :  (\arbno{\LOC} \to \CC) \to \arbno{\EXP} \to \CC$\\$
  324. \fun{tievals} =$\\
  325.  \go{1}$\lambda\psi\arbno{\epsilon}\sigma\:.\:
  326.    $\=$\#\arbno{\epsilon}=0\rightarrow\psi\langle\:\rangle\sigma,$\\
  327.     \>$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow\fun{tievals}\,
  328.        $\=$(\lambda\arbno{\alpha}\:.\:\psi(\langle\fun{new}\:\sigma\:\vert\:\LOC\rangle
  329.                      \:\S\:\arbno{\alpha}))$\\
  330.     \>  \>$(\arbno{\epsilon}\drop 1)$\\
  331.     \>  \>$(\fun{update}(\fun{new}\:\sigma\:\vert\:\LOC)
  332.                      (\arbno{\epsilon}\elt 1)
  333.                  \sigma),$\\
  334.     \>$\go{1}\wrong{out of memory}\sigma
  335. \end{semfun}
  336. \begin{semfun}
  337. \fun{tievalsrest}   :  (\arbno{\LOC} \to \CC) \to \arbno{\EXP} \to \NAT \to \CC$\\$
  338. \fun{tievalsrest} =$\\
  339.  \go{1}$\lambda\psi\arbno{\epsilon}\nu\:.\:\fun{list}\:
  340.    $\=$(\fun{dropfirst}\:\arbno{\epsilon}\nu)$\\
  341.     \>$(\fun{single}(\lambda\epsilon\:.\:\fun{tievals}\:\psi\:
  342.            ((\fun{takefirst}\:\arbno{\epsilon}\nu)\:\S\:\langle\epsilon\rangle)))
  343. \end{semfun}
  344. \begin{semfun}
  345. \fun{dropfirst} =
  346.  \lambda l n \:.\:  n=0 \rightarrow l, \fun{dropfirst}\,(l \drop 1)(n - 1)
  347. \end{semfun}
  348. \begin{semfun}
  349. \fun{takefirst} =
  350.  \lambda l n \:.\: n=0 \rightarrow \langle\:\rangle,
  351.      \langle l \elt 1\rangle\:\S\:(\fun{takefirst}\,(l \drop 1)(n - 1))
  352. \end{semfun}
  353. \begin{semfun}
  354. \fun{truish}        :  \EXP \to \TRU$\\$
  355. \fun{truish} =
  356.   \lambda\epsilon\:.\:
  357.      (\epsilon = \fun{false}\vee\epsilon = \fun{null})\rightarrow
  358.           \fun{false},
  359.           \fun{true}
  360. \end{semfun}
  361. \begin{semfun}
  362. \fun{permute}       :  \arbno{\Exp} \to \arbno{\Exp}
  363.     \hbox{\qquad [implementation-dependent]}
  364. \end{semfun}
  365. \begin{semfun}
  366. \fun{unpermute}     :  \arbno{\EXP} \to \arbno{\EXP}
  367.     \hbox{\qquad [inverse of \fun{permute}]}
  368. \end{semfun}
  369. \begin{semfun}
  370. \fun{applicate}     :  \EXP \to \arbno{\EXP} \to \EC \to \CC$\\$
  371. \fun{applicate} =$\\
  372.  \go{1}$\lambda\epsilon\arbno{\epsilon}\kappa\:.\:
  373.    $\=$\epsilon\:\elem\:\FUN\rightarrow(\epsilon\:\vert\:\FUN\elt 2)\arbno{\epsilon}\kappa,
  374.           \wrong{bad procedure}
  375. \end{semfun}
  376. \begin{semfun}
  377. \fun{onearg}      :  (\EXP \to \EC \to \CC) \to (\arbno{\EXP} \to \EC \to \CC)$\\$
  378. \fun{onearg} =$\\
  379.  \go{1}$\lambda\zeta\arbno{\epsilon}\kappa\:.\:
  380.    $\=$\#\arbno{\epsilon}=1\rightarrow\zeta(\arbno{\epsilon}\elt 1)\kappa,$\\
  381.     \>$\go{1}\wrong{wrong number of arguments}
  382. \end{semfun}
  383. \begin{semfun}
  384. \fun{twoarg}      :  (\EXP \to \EXP \to \EC \to \CC) \to (\arbno{\EXP} \to \EC \to \CC)$\\$
  385. \fun{twoarg} =$\\
  386.  \go{1}$\lambda\zeta\arbno{\epsilon}\kappa\:.\:
  387.    $\=$\#\arbno{\epsilon}=2\rightarrow\zeta(\arbno{\epsilon}\elt 1)(\arbno{\epsilon}\elt 2)\kappa,$\\
  388.     \>$\go{1}\wrong{wrong number of arguments}
  389. \end{semfun}
  390. \begin{semfun}
  391. \fun{list}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  392. \fun{list} =$\\
  393.  \go{1}$\lambda\arbno{\epsilon}\kappa\:.\:
  394.    $\=$\#\arbno{\epsilon}=0\rightarrow\fun{send}\:\fun{null}\:\kappa,$\\
  395.     \>$\go{1}\fun{list}\,(\arbno{\epsilon}\drop 1)
  396.              (\fun{single}(\lambda\epsilon\:.\:
  397.                    \fun{cons}\langle\arbno{\epsilon}\elt 1,\epsilon\rangle\kappa))
  398. \end{semfun}
  399. \begin{semfun}
  400. \fun{cons}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  401. \fun{cons} =$\\
  402.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\sigma\:.\:
  403.    $\=$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  404.     \> \go{1}
  405.         \=$(\lambda\sigma^\prime\:.\:
  406.            $\=$\fun{new}\:\sigma^\prime\:\elem\:\LOC\rightarrow$\\
  407.     \>  \>  \>$\go{1}\fun{send}\,
  408.            $\=$($\=$\langle\fun{new}\:\sigma\:\vert\:\LOC,
  409.                         \fun{new}\:\sigma^\prime\:\vert\:\LOC,
  410.          \fun{true}\rangle$\\
  411.                 \>  \>  \>  \>  \>$\hbox{ \rm in }\EXP)$\\
  412.     \>  \>  \>  \>$\kappa$\\
  413.     \>  \>  \>  \>$(\fun{update}(\fun{new}\:\sigma^\prime\:\vert\:\LOC)
  414.                          \epsilon_2
  415.                      \sigma^\prime),$\\
  416.     \>  \>  \>$\go{1}\wrong{out of memory}\sigma^\prime)$\\
  417.     \>  \>$(\fun{update}(\fun{new}\:\sigma\:\vert\:\LOC)\epsilon_1\sigma),$\\
  418.     \>$\go{1}\wrong{out of memory}\sigma)
  419. \end{semfun}
  420. \begin{semfun}
  421. \fun{less}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  422. \fun{less} =$\\
  423.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  424.    $\=$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
  425.     \>$\go{1}\fun{send}\,
  426.            (\epsilon_1\:\vert\:\NUM<\epsilon_2\:\vert\:\NUM\rightarrow
  427.                \fun{true},
  428.            \fun{false})
  429.            \kappa,$\\
  430.     \>$\go{1}\wrong{non-numeric argument to \ide{<}})
  431. \end{semfun}
  432. \begin{semfun}
  433. \fun{add}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  434. \fun{add} =$\\
  435.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  436.    $\=$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
  437.     \>$\go{1}\fun{send}\,
  438.        $\=$((\epsilon_1\:\vert\:\NUM+\epsilon_2\:\vert\:\NUM)\hbox{ \rm in }\EXP)
  439.            \kappa,$\\
  440.     \>$\go{1}\wrong{non-numeric argument to \ide{+}})
  441. \end{semfun}
  442. \begin{semfun}
  443. \fun{car}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  444. \fun{car} =$\\
  445.  \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
  446.    $\=$\epsilon\:\elem\:\PAI\rightarrow
  447.           \fun{hold}\, (\epsilon\:\vert\:\PAI\elt 1) \kappa,$\\
  448.     \>$\go{1}\wrong{non-pair argument to \ide{car}})
  449. \end{semfun}
  450. \begin{semfun}
  451. \fun{cdr}          :  \arbno{\EXP} \to \EC \to \CC %$\\$
  452. \hbox{\qquad [similar to \fun{car}]}
  453. \end{semfun}
  454. \begin{semfun}
  455. \fun{setcar}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  456. \fun{setcar} =$\\
  457.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  458.    $\=$\epsilon_1\:\elem\:\PAI\rightarrow$\\
  459.     \>$(\epsilon_1\:\vert\:\PAI\elt 3)\rightarrow
  460.           \fun{assign}\,$\=$(\epsilon_1\:\vert\:\PAI\elt 1)$\\
  461.     \>                         \>$\epsilon_2$\\
  462.     \>                            \>$(\fun{send}\:\fun{unspecified}\:\kappa),$\\
  463.     \>$\wrong{immutable argument to \ide{set-car!}},$\\
  464.     \>$\wrong{non-pair argument to \ide{set-car!}})
  465. \end{semfun}
  466. \begin{semfun}
  467. \fun{eqv}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  468. \fun{eqv} =$\\
  469.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  470.    $\=$(\epsilon_1\:\elem\:\MSC\wedge\epsilon_2\:\elem\:\MSC)\rightarrow$\\
  471.     \>$\go{1}\fun{send}\,
  472.        $\=$(\epsilon_1\:\vert\:\MSC = \epsilon_2\:\vert\:\MSC\rightarrow\fun{true},
  473.             \fun{false})\kappa,$\\
  474.     \>$(\epsilon_1\:\elem\:\SYM\wedge\epsilon_2\:\elem\:\SYM)\rightarrow$\\
  475.     \>$\go{1}\fun{send}\,
  476.        $\=$(\epsilon_1\:\vert\:\SYM = \epsilon_2\:\vert\:\SYM\rightarrow\fun{true},
  477.             \fun{false})\kappa,$\\
  478.     \>$(\epsilon_1\:\elem\:\CHR\wedge\epsilon_2\:\elem\:\CHR)\rightarrow$\\
  479.     \>$\go{1}\fun{send}\,
  480.        $\=$(\epsilon_1\:\vert\:\CHR = \epsilon_2\:\vert\:\CHR \rightarrow\fun{true},
  481.             \fun{false})\kappa,$\\
  482.     \>$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
  483.     \>$\go{1}\fun{send}\,
  484.        $\=$(\epsilon_1\:\vert\:\NUM=\epsilon_2\:\vert\:\NUM\rightarrow\fun{true},
  485.             \fun{false})\kappa,$\\
  486.     \>$(\epsilon_1\:\elem\:\PAI\wedge\epsilon_2\:\elem\:\PAI)\rightarrow$\\
  487.     \>$\go{1}\fun{send}\,
  488.        $\=$($\=$(\lambda{p_1}{p_2}\:.\:
  489.                 ($\=$({p_1}\elt 1) = ({p_2}\elt 1)\wedge$\\
  490.     \>  \>   \>   \>$({p_1}\elt 2) = ({p_2}\elt 2))
  491.                      \rightarrow\fun{true},$\\
  492.     \>  \>   \>   \>$\go{1}\fun{false})$\\
  493.     \>  \>   \>$(\epsilon_1\:\vert\:\PAI)$\\
  494.     \>  \>   \>$(\epsilon_2\:\vert\:\PAI))$\\
  495.     \>  \>$\kappa,$\\
  496.     \>$(\epsilon_1\:\elem\:\VEC\wedge\epsilon_2\:\elem\:\VEC)\rightarrow
  497. %\fun{send}\,
  498. %       $\=$((\#(\epsilon_1\:\vert\:\VEC)=\#(\epsilon_2\:\vert\:\VEC)
  499. %         \wedge\hbox{\rm Y}(\lambda\fun{loop}\:.\:\lambda\fun{v1}\fun{v2}\:.\:
  500. %       $\=$\#\fun{v1}=0\rightarrow\fun{true},$\\
  501. %    \>  \>  \>$(\fun{v1}\elt 1) = (\fun{v2}\elt 1)\rightarrow
  502. %       \fun{loop}(\fun{v1}\drop 1)(\fun{v2}\drop 1),$\\
  503. %    \>  \>  \>$\go{1}\fun{false})(\epsilon_1\:\vert\:\VEC)(\epsilon_2\:\vert\:\VEC))
  504. %          \rightarrow\fun{true},$\\
  505. %    \>  \>$\go{1}\fun{false})\kappa
  506. \ldots,$\\
  507.     \>$(\epsilon_1\:\elem\:\STR\wedge\epsilon_2\:\elem\:\STR)\rightarrow
  508. %\fun{send}\,
  509. %       $\=$((\#(\epsilon_1\:\vert\:\STR)=\#(\epsilon_2\:\vert\:\STR)\wedge
  510. %    \hbox{\rm Y}(\lambda\fun{loop}\:.\:\lambda\fun{v1}\fun{v2}\:.\:
  511. %       $\=$\#\fun{v1}=0\rightarrow\fun{true},$\\
  512. %    \>  \>  \>$(\fun{v1}\elt 1) = (\fun{v2}\elt 1)\rightarrow
  513. %     \fun{loop}(\fun{v1}\drop 1)(\fun{v2}\drop 1),$\\
  514. %    \>  \>  \>$\go{1}\fun{false})(\epsilon_1\:\vert\:\STR)(\epsilon_2\:\vert\:\STR))
  515. %      \rightarrow\fun{true},$\\
  516. %    \>  \>$\go{1}\fun{false})\kappa
  517. \ldots,$\\
  518.     \>$(\epsilon_1\:\elem\:\FUN\wedge\epsilon_2\:\elem\:\FUN)\rightarrow$\\
  519.     \>$\go{1}\fun{send}\,
  520.        $\=$((\epsilon_1\:\vert\:\FUN\elt 1) = (\epsilon_2\:\vert\:\FUN\elt 1)
  521.                \rightarrow\fun{true},
  522.                       \fun{false})$\\
  523.     \>  \>$\kappa,$\\
  524.     \>$\go{1}\fun{send}\,\:\fun{false}\:\kappa)
  525. \end{semfun}
  526. \begin{semfun}
  527. \fun{apply}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  528. \fun{apply} =$\\
  529.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  530.    $\=$\epsilon_1\:\elem\:\FUN\rightarrow
  531.          \fun{valueslist}\,\langle\epsilon_2\rangle
  532.             (\lambda\arbno{\epsilon}\:.\:\fun{applicate}\:\epsilon_1\arbno{\epsilon}\kappa),$\\
  533.     \>$\go{1}\wrong{bad procedure argument to \ide{apply}})
  534. \end{semfun}
  535. \begin{semfun}
  536. \fun{valueslist}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  537. \fun{valueslist} =$\\
  538.  \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
  539.    $\=$\epsilon\:\elem\:\PAI\rightarrow$\\
  540.     \>$\go{1}\fun{cdr}
  541.          $\=$\langle\epsilon\rangle$\\
  542.     \>    \>$(\lambda\arbno{\epsilon}\:.\:
  543.               $\=$\fun{valueslist}\:$\\
  544.     \>    \>       \>$\arbno{\epsilon}$\\
  545.     \>    \>       \>$(\lambda\arbno{\epsilon}\:.\:\fun{car}\langle\epsilon\rangle
  546.         (\fun{single}(\lambda\epsilon\:.\:
  547.           \kappa(\langle\epsilon\rangle\:\S\:\arbno{\epsilon}))))),$\\
  548.     \>$\epsilon = \fun{null}\rightarrow\kappa\langle\:\rangle,$\\
  549.     \>$\go{1}\wrong{non-list argument to \ide{values-list}})
  550. \end{semfun}
  551. \begin{semfun}
  552. \fun{cwcc}          :  \arbno{\EXP} \to \EC \to \CC
  553.     \hbox{\qquad [\ide{call-with-current-continuation}]}$\\$
  554. \fun{cwcc} =$\\
  555.  \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
  556.    $\=$\epsilon\:\elem\:\FUN\rightarrow$\\
  557.     \>$\go{1}(\lambda\sigma\:.\:
  558.        $\=$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  559.     \>  \>$\go{1}\fun{applicate}\:
  560.        $\=$\epsilon$\\
  561.     \>  \>  \>$\langle\langle\fun{new}\:\sigma\:\vert\:\LOC,
  562.                  \lambda\arbno{\epsilon}\kappa^\prime\:.\:
  563.                  \kappa\arbno{\epsilon}\rangle
  564.               \hbox{ \rm in }\EXP\rangle$\\
  565.     \>  \>  \>$\kappa$\\
  566.     \>  \>  \>$(\fun{update}\,
  567.             $\=$(\fun{new}\:\sigma\:\vert\:\LOC)$\\
  568.     \>    \>  \>     \>$\fun{unspecified}$\\
  569.     \>    \>  \>     \>$\sigma),$\\
  570.     \>  \>$\go{1}\wrong{out of memory}\,\sigma),$\\
  571.     \>$\go{1}\wrong{bad procedure argument})
  572. \end{semfun}
  573. \egroup  % end smallish
  574. \egroup
  575.